Termination w.r.t. Q proof of /tmp/tmpkTlxYe/Ex49_GM04

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(div(minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
activate(n__0) → 0
activate(n__s(X)) → s(X)
activate(X) → X

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(div(minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
activate(n__0) → 0
activate(n__s(X)) → s(X)
activate(X) → X

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

DIV(s(X), n__s(Y)) → GEQ(X, activate(Y))
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
ACTIVATE(n__s(X)) → S(X)
MINUS(n__0, Y) → 0¹
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
IF(true, X, Y) → ACTIVATE(X)
DIV(s(X), n__s(Y)) → MINUS(X, activate(Y))
IF(false, X, Y) → ACTIVATE(Y)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
ACTIVATE(n__0) → 0¹
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
DIV(s(X), n__s(Y)) → DIV(minus(X, activate(Y)), n__s(activate(Y)))
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(div(minus(X, activate(Y)), n__s(activate(Y)))), n__0)
GEQ(n__s(X), n__s(Y)) → GEQ(activate(X), activate(Y))
MINUS(n__s(X), n__s(Y)) → MINUS(activate(X), activate(Y))

The TRS R consists of the following rules:

minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(div(minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
activate(n__0) → 0
activate(n__s(X)) → s(X)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

DIV(s(X), n__s(Y)) → GEQ(X, activate(Y))
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
ACTIVATE(n__s(X)) → S(X)
MINUS(n__0, Y) → 0¹
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
IF(true, X, Y) → ACTIVATE(X)
DIV(s(X), n__s(Y)) → MINUS(X, activate(Y))
IF(false, X, Y) → ACTIVATE(Y)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
ACTIVATE(n__0) → 0¹
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
DIV(s(X), n__s(Y)) → DIV(minus(X, activate(Y)), n__s(activate(Y)))
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(div(minus(X, activate(Y)), n__s(activate(Y)))), n__0)
GEQ(n__s(X), n__s(Y)) → GEQ(activate(X), activate(Y))
MINUS(n__s(X), n__s(Y)) → MINUS(activate(X), activate(Y))

The TRS R consists of the following rules:

minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(div(minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
activate(n__0) → 0
activate(n__s(X)) → s(X)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 3 SCCs with 13 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GEQ(n__s(X), n__s(Y)) → GEQ(activate(X), activate(Y))

The TRS R consists of the following rules:

minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(div(minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
activate(n__0) → 0
activate(n__s(X)) → s(X)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

GEQ(n__s(X), n__s(Y)) → GEQ(activate(X), activate(Y))

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25,35]:

POL(n__0) = 4
POL(activate(x₁)) = 1 + (2)x_1
POL(s(x₁)) = 4 + (3)x_1
POL(n__s(x₁)) = 4 + (3)x_1
POL(0) = 4
POL(GEQ(x₁, x₂)) = (3)x_2

The value of delta used in the strict ordering is 9.
The following usable rules [17] were oriented:

s(X) → n__s(X)
0 → n__0
activate(n__s(X)) → s(X)
activate(n__0) → 0
activate(X) → X

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(div(minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
activate(n__0) → 0
activate(n__s(X)) → s(X)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

MINUS(n__s(X), n__s(Y)) → MINUS(activate(X), activate(Y))

The TRS R consists of the following rules:

minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(div(minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
activate(n__0) → 0
activate(n__s(X)) → s(X)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

MINUS(n__s(X), n__s(Y)) → MINUS(activate(X), activate(Y))

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25,35]:

POL(n__0) = 0
POL(MINUS(x₁, x₂)) = (3)x_2
POL(activate(x₁)) = x_1
POL(s(x₁)) = 3 + (4)x_1
POL(n__s(x₁)) = 3 + (4)x_1
POL(0) = 0

The value of delta used in the strict ordering is 9.
The following usable rules [17] were oriented:

s(X) → n__s(X)
0 → n__0
activate(n__s(X)) → s(X)
activate(n__0) → 0
activate(X) → X

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(div(minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
activate(n__0) → 0
activate(n__s(X)) → s(X)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

DIV(s(X), n__s(Y)) → DIV(minus(X, activate(Y)), n__s(activate(Y)))

The TRS R consists of the following rules:

minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(div(minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
activate(n__0) → 0
activate(n__s(X)) → s(X)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

DIV(s(X), n__s(Y)) → DIV(minus(X, activate(Y)), n__s(activate(Y)))

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25,35]:

POL(minus(x₁, x₂)) = 2
POL(n__0) = 1/2
POL(DIV(x₁, x₂)) = (4)x_1 + (4)x_2
POL(s(x₁)) = 4 + (3)x_1
POL(activate(x₁)) = 4
POL(n__s(x₁)) = 13/4
POL(0) = 5/4

The value of delta used in the strict ordering is 8.
The following usable rules [17] were oriented:

minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
0 → n__0

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(div(minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
activate(n__0) → 0
activate(n__s(X)) → s(X)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.